Lean 4
←
Lean 3
Lean
のバージョン4系
コードの書き方が
Lean 3
からかなり変わっている
論文系
Lean papers
Lean日本語コミュニティ
LEAN JA
GitHub:
lean-ja · GitHub
Discordへの招待リンクがある
Lean 4のドキュメント、学習回りは下記ページ
Lean 4を学ぶ
Lean 4でHello World
Lean 4 基礎
Lean 4 入出力
Lean 4 関数型プログラミング
Lean 4 デバッグ
#print
Lean 4 マクロ
Web上で実行できるものもある
Lean 4 Web
Natural number game
ProofWidgets4
PatrickMassot/leanblueprint: plasTeX plugin to build formalization blueprints.
Mathlib
SciLean
LeanExplore
PhysLean
HEPLean/PhysLean: A project to digitalise results from physics into Lean.
Leanで証明している事例
iehality/lean4-logic at system-modal-doc
Lean 4で
様相論理
を形式化している
Leanと様相論理
Lean4 Logic Formalization - Logic Formalization in Lean 4
Gödel's First Incompleteness Theorem - Logic Formalization in Lean 4
Lean 4 ログ
参考
プログラミング言語Lean 4の現状 - 檜山正幸のキマイラ飼育記 (はてなBlog)
Learning Lean 4
#Lean